Nuprl Lemma : fun-connected_wf
11,40
postcript
pdf
T
:Type,
f
:(
T
T
),
x
,
y
:
T
.
y
is
f
*(
x
)
latex
Definitions
Type
,
t
T
,
s
=
t
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
y
=
f
*(
x
) via
L
,
type
List
,
x
:
A
B
(
x
)
,
,
x
:
A
.
B
(
x
)
,
y
is
f
*(
x
)
Lemmas
fun-path
wf
origin
T:Type, f:(T
T), x, y:T. y is f*(x) 
T:Type, f:(TT), x, y:T. y is f*(x) TB(x)x:A. B(x)
B(x)
x:A. B(x)